es:event_system{i:l}, x,y:es-E(es).
(x rel_plus(es-E(es); (x,y. ((first(y))) c (x = pred(y)))) y)  (loc(x) = loc(y)  Id) 

latex

Definitions

x f y, rel_plus(T; R), event_system{i:l}, t  T, x:AB(x), x:A  B(x), loc(e), Id, s = t, es-pred?(es), pred(e), es-E(es), first(e), b, A, A c B, x.A(x), rel_exp(T; R; n), f(a), P  Q, x:A. B(x), , #$n, n - m, a < b, void, False, A  B, {x:A| B(x)} , , , Type, prop{i:l}, P  Q, x:A. B(x), b, , (i = j), P  Q, Unit, left + right, guard(T), sq_type(T), sqequal(s; t), P  Q, decidable(P), es-first(es; e), -n, n + m

Lemmas

nat plus inc, Id wf, es-loc wf, es-loc-pred, nat plus wf, nat plus properties, le wf, decidable int equal, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, rel exp wf, not wf, assert wf, first wf, pred wf, es-pred? wf, es-E wf, event system wf